Nuprl Definition : update-spec
11,40
postcript
pdf
update-spec(
ds
;
da
)
== fpf((
:Knd
Id);
== fpf(
kz
.((
n
:
(decl-state(
ds
)
ma-valtype(
da
; (
kz
.1))
fpf-cap(
ds
; id-deq; (
kz
.2); void))) List)
== fpf(
)
latex
Definitions
fpf(
A
;
a
.
B
(
a
))
,
Knd
,
Id
,
type
List
,
x
:
A
B
(
x
)
,
,
decl-state(
ds
)
,
x
:
A
B
(
x
)
,
ma-valtype(
da
;
k
)
,
t
.1
,
fpf-cap(
f
;
eq
;
x
;
z
)
,
id-deq
,
t
.2
,
void
FDL editor aliases
update-spec
origin